f:(RealizerRealizer), A:Realizer. Rtransform(f;A)  Realizer 

latex

Definitions	tt, ff, Rplus-right(x1), Rplus-left(x1), Rplus?(x1), if b then t else f fi , Y, x. t(x), Rtransform(f;A), t  T, x:A. B(x), x(s), Unit, Realizer, Rrframe(loc;x;L), Rbframe(loc;k;L), Raframe(loc;k;L), Rpre(loc;ds;a;p;P), Rsends(ds;knd;T;l;dt;g), Reffect(loc;ds;knd;T;x;f), Rsframe(lnk;tag;L), Rframe(loc;T;x;L), Rinit(loc;T;x;v), left  right, Rnone(),
Lemmas	es realizer wf, Rrframe wf, Rbframe wf, Raframe wf, Rpre wf, Rsends wf, Reffect wf, Rsframe wf, Rframe wf, Rinit wf, R-plus wf, Rnone wf, bool wf, finite-prob-space wf, decl-type wf, decl-state wf, fpf wf, IdLnk wf, Knd wf, rationals wf, Id wf, unit wf